2020-05-13 16:30:9 (GMT)
This problem is (kind of) of the form .
Now this is fairly complicated and creates tons of clauses.
This makes Zipperposition fail on this problem with any configuration (and Vampire as well).
I was wondering if superposition veterans (@Stephan Schulz, @Jasmin Blanchette , @Giles , @Sophie ) have an idea how this problem is solved in FO case.
2020-05-13 16:30:28 (GMT)
I also forgot to mention that what makes this problem horrible is the amout of applied variables that appear
2020-05-13 16:40:59 (GMT)
isn't that the poster child for non-clausal superposition?
2020-05-13 16:53:2 (GMT)
Vampire HOL can solve SEU909 using a strategy that switches off most higher-order inferences.
2020-05-13 16:57:44 (GMT)
Ok, I tried it on SystemOnTPTP and got timeout in 180s
2020-05-13 17:4:0 (GMT)
That is strange. The version on SystemOnTPTP would be last year's version, but even that should be able to find a proof.
Sorry, the proof output is not very readable!
2020-05-13 17:33:36 (GMT)
On the FOF level, isn't that a trivial tautology? E would negate it, and then (hopefully) uncover the contradiction.
2020-05-13 17:51:50 (GMT)
Stephan Schulz said:
On the FOF level, isn't that a trivial tautology? E would negate it, and then (hopefully) uncover the contradiction.
This is the whole point. It is a very trivial tautology, but if is complicated, clausification will obfuscate the problem significantly, making it very hard to find the contradiction
2020-05-13 18:41:6 (GMT)
Indeed, I've seen cases like this in Isabelle where proving P x using P x with Sledgehammer would fail. Due to clausification. We'd get like 1000+ clauses. But I guess this was because we had hooked a naive clausifer on top of Metis.
2020-05-13 18:55:43 (GMT)
So lazy clausification as you've implemented in Zipperposition doesn't help?
2020-05-13 19:6:27 (GMT)
unfortunately no... there are not many equivalences in that problem that stay intact
2020-05-13 19:49:27 (GMT)
and that's where tableau approaches like LeanCop (and siblings) shine, sadly they're always terrible at equality reasoning.
2020-05-13 20:22:15 (GMT)
How about making lazy clausification even lazier?
2020-05-13 20:39:13 (GMT)
What do you mean by that?
2020-05-13 20:39:37 (GMT)
Interestingly, E solves it fast, when I remove lambdas because it does better formula renaming than Zip
2020-05-13 20:52:0 (GMT)
Petar Vukmirovic said:
What do you mean by that?
well I guess you could make some CNF rules into inference rules, not simplifications, so that has time to be matched as is before it's atomized into clauses.
2020-05-14 6:53:38 (GMT)
Or, you keep them as simplifications but you apply them later in the loop, e.g. on the given clause after performing all inferences?
2020-05-14 9:43:55 (GMT)
In the end, it was the matter of heuristics...
I found a configuration that uses lazy clausification as inference (instead of simplification) rules and manages to do correct superposition (as witnessed by the following proof):
tff('8', plain,
(!!((^[Y0 : (a > $o) > $o]:
((Y0((^[Y1 : a]: $false)) &
(!!((^[Y1 : a > $o]:
(Y0(Y1) =>
(!!((^[Y2 : a]:
('#sk1'(Y2) =>
Y0((^[Y3 : a]: (Y1(Y3) | (Y2 = Y3))))))))))))) =>
Y0('#sk1'))))),
inference('lazy_cnf_and', [status(thm)], ['7'])).
tff('10', plain,
![X1 : a > $o]:
~ ((!!((^[Y0 : (a > $o) > $o]:
((Y0((^[Y1 : a]: $false)) &
(!!((^[Y1 : a > $o]:
(Y0(Y1) =>
(!!((^[Y2 : a]:
(X1(Y2) =>
Y0((^[Y3 : a]: (Y1(Y3) | (Y2 = Y3))))))))))))) =>
Y0(X1)))))&
(!!((^[Y0 : a]: (X1(Y0) => '#sk89'(Y0)))))&
(!!((^[Y0 : a > $o]:
((cA(Y0) & (!!((^[Y1 : a]: (X1(Y1) => Y0(Y1)))))) =>
(cA(Y0) & (!!((^[Y1 : a]: ('#sk1'(Y1) => Y0(Y1))))))))))),
inference('lazy_cnf_forall', [status(thm)], ['9'])).
tff('11', plain,
~ ($true&(!!((^[Y0 : a]: ((^[Y1 : a]: '#sk1'(Y1))(Y0) => '#sk89'(Y0)))))&
(!!((^[Y0 : a > $o]:
((cA(Y0) &
(!!((^[Y1 : a]: ((^[Y2 : a]: '#sk1'(Y2))(Y1) => Y0(Y1)))))) =>
(cA(Y0) & (!!((^[Y1 : a]: ('#sk1'(Y1) => Y0(Y1))))))))))),
inference('sup-', [status(thm)], ['8', '10'])).
2020-05-14 10:18:8 (GMT)
2020-05-14 10:18:23 (GMT)
It is not well performing as it is to expect, but in some corner cases (such as this one) it comes in handy
2020-05-14 11:8:37 (GMT)
I found another configuration that might help if you use VCNF-like algo : very eager renaming helps to factor out common formulas in premise and conclusion:
When I run lazy cnf in simplification mode with renaming threshold set to 2 the problem is solved fast
2020-05-14 16:5:19 (GMT)
We've been meaning to implement 'formula sharing' in Vampire for a while e.g. in parsing make syntacticly equivalent formulas pointer-equivalent like we do with terms. This would make a difference here. We mention it in the VCNF paper.
2020-05-14 17:55:56 (GMT)
Not to give the Denizens of the Night any ideas, but E actually encodes FOF formulas as terms (which implies sharing).
2020-05-14 19:45:46 (GMT)
And the logical conclusion is to also encode types as terms! Everything is a term! :slight_smile:
2020-05-14 23:3:19 (GMT)
Interesting, @Ahmed B was just suggesting doing something like that by just using his existing encoding of formulas as terms for formulas in terms. But to get full benefit we need sharing to be up to AC and we just support C.